A, B:Realizer. R-interface-compat(A;B)  Prop 

latex

Definitions	x:A. B(x), t  T, Prop, R-interface-compat(A;B), if b t else f fi, let x = a in b(x), p  q, isrcv(k), lnk(k), tag(k), P  Q, true, isl(x), 1of(t), outl(x), 2of(t), false, x. t(x), , Unit, P  Q, P & Q, Knd, x(s), , rcv(l,tg), locl(a)
Lemmas	Rsends? wf, bool wf, eqtt to assert, Reffect? wf, true wf, Reffect-knd wf, ifthenelse wf, eq lnk wf, Rsends-l wf, subtype rel wf, fpf-cap wf, Id wf, Rsends-dt wf, id-deq wf, Reffect-T wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Rsends-knd wf, Rsends-T wf, es realizer wf